In computer systems, and particularly networked computer systems, it is common for a first computer system to download and execute a program from a second computer system. During its execution, the program might access private data of the first computer. Generally, the first computer might permit the program to read and write such private data. Moreover, the first computer might permit the program to read and send public data back to the second computer. The first computer, however, wants to ensure that the program does not send private data back to the second computer along with the public data. So, the program must have a secure information flow, that is, the behavior of the program must not reveal anything about the private data of the first computer, either by the public data that is returned to the second computer or by not returning the public data at all.
Consequently, the problem of determining whether the information flow of a program is secure has given rise to two general approaches at a solution, type systems and data flow analyses. Type systems associate a type or a security level with each expression and statement in the program. Some statements may not type check: for example an assignment statement "x:=E", which assigns the value of expression E to variable x, type checks only if the type of expression E is less than or equal to the type of variable x (i.e., type(E).ltoreq.type(x)). For a program to be secure, every statement must type check.
The data flow analysis approach analyzes the data flow of a program using standard compiler techniques. For example, the program "v:=v+h; v:=0", where h is a private variable, and v is a public variable, is transformed into another program with a variable vv denoting the set of variables that may contribute to the value of the variable v and with a variable hh denoting the set of variables that may contribute to the value of the variable h. The exemplary program becomes "vv:=vv.orgate.hh; vv:={ }", where ".orgate." denotes set union and "{ }" denotes the empty set. Standard compiler techniques then infer that the program ends with "vv is { }", which means that the final value of v does not depend upon any other variables, especially not upon the value of h. Hence, the data flow analysis will certify this program.
Both the type system and data flow analyses approaches have been proven sound; that is, these methods do not give false positives. Therefore, a program certified as secure is truly secure. Both approaches, however, are too coarse and reject too many programs that are actually secure, i.e., they produce too many false negatives. Known type systems, for instance, will reject any program with an insecure sub-component and thus produce a false negative. For example, the type system method will incorrectly reject the program "v:=h; v:=0" because of the "v:=h" sub-component, even though the final value of v does not depend on h. The data flow analysis approach will reject some secure programs because the approach does not detect that a particular operator in the program will make the final value of v independent of the value of h. For example, the data flow method will reject the secure program "v:=h; v:=v-h", although the program always terminates with v=0.
Hence, a more fine grained method and apparatus are needed that can properly certify programs with secure information flow that previous implementations reject.